$\forall$$T$:Type, ${\it eq}$:($T$$\rightarrow$$T$$\rightarrow\mathbb{B}$). eq\_seq(${\it eq}$) $\in$ ($k$:$\mathbb{N}$ $\times$ (\{0..$k$$^{-}$\}$\rightarrow$$T$))$\rightarrow$($k$:$\mathbb{N}$ $\times$ (\{0..$k$$^{-}$\}$\rightarrow$$T$))$\rightarrow\mathbb{B}$